A:Type, l:A List, x:A. (x.l)  A List 

latex

Definitions	t  T, b, x:A. B(x), A List, ||as||, i<j, ij, P  Q, P  Q, P & Q, P  Q
Lemmas	assert of lt int, non neg length, assert wf, lt int wf, length wf1